\documentclass[orivec]{llncs}

\usepackage{intestazione2}
\usepackage{times}
\usepackage{macro}
%\usepackage{geometry}





\begin{document}

%
\frontmatter          
\pagestyle{headings}  
%
\mainmatter           

\title{Disciplined Structured Communications with Disciplined Adaptation (Extended Version)\thanks{Revision of \today. An extended abstract will appear in the Proceedings of the \href{http://www.acm.org/conferences/sac/sac2013/}{28th ACM Symposium On Applied Computing (SAC'13)}, \copyright ACM.}}


 \author{Cinzia Di Giusto\inst{1} \and Jorge A. P\'erez\inst{2}}

\institute{
Universit\'e d'Evry - Val d'Essonne, IBISC, Evry, France
\and 
CITI - Dept. of Computer Science, FCT New University of Lisbon, Portugal
}
\maketitle      
\begin{abstract}
\emph{Session types} offer a powerful
%have been intensively studied as 
%formal models 
 type-the\-o\-ret\-ic foundation for the analysis of 
%complex scenarios of 
structured communications, as commonly found in serv\-ice-oriented systems.
They are defined upon core programming calculi which offer only limited support 
%lack explicit constructs 
for expressing adaptation and evolvability requirements.
This is unfortunate, as serv\-ice\--ori\-ented systems are increasingly being deployed upon %open, 
highly dynamic infrastructures in which such requirements are 
%fundamental 
central concerns.
%central in ensuring reliable system operation. % and business agility.
In previous work, we developed a process calculi framework of \emph{adaptable processes},
in which concurrent processes can be replaced,  suspended, or discarded at runtime.
%as an attempt to enhance process calculi specifications with evolvability concerns.
In this paper, we %extend %integrate adaptable processes into 
propose a session types discipline for a calculus with adaptable processes. 
%The resulting 
Our framework offers an alternative for integrating runtime adaptation mechanisms  in 
the analysis of structured communications.
We show that well-typed processes enjoy \emph{consistency}:
communicating behavior is never interrupted by evolvability actions. 
\end{abstract}

\input{intro}

\input{syntax}

\input{types}
%

\input{theorems}

\input{exserver}

\input{interface}

\input{conclud}

\bibliographystyle{abbrv}
\bibliography{referen}

\appendix
\section{Proofs}
\input{appendix}
\input{derivation}



\end{document}